M1, M2:MsgA. M1  M2  (k:Knd, l:IdLnk. M2.bframe(k sends on l)  M1.bframe(k sends on l)) 

latex

Definitions	x:AB(x), A & B, t  T, P  Q, x:A. B(x), f  g, Id, x:AB(x), True, Knd, IdLnk, type List, f(x), <a,b>, s = t, IdLnkDeq, T, Type, EqDecider(T), deq-member(eq;x;L), Prop, , b, x.A(x), x. t(x), Top, a:A fp B(a), KindDeq, x  dom(f), z != f(x)  P(a;z), P & Q, Valtype(da;k), MsgA, M1  M2, M.bframe(k sends on l)
Lemmas	ma-bframe wf, ma-sub wf, msga wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, Knd wf, assert wf, bool wf, deq-member wf, squash wf, true wf, deq wf, IdLnk wf, idlnk-deq wf